『The paradox of trees in type theory』
https://www.researchgate.net/publication/225267298_The_paradox_of_trees_in_type_theory
1. どんなもの？
2. 先行研究と比べてどこがすごい？
3. 技術や手法のキモはどこ？
4. どうやって有効だと検証した？
5. 議論はある？
6. 次に読むべき論文は？
不動点演算子(fixed-point orerator)
W型(W-type)
extensional equality(外延的等価性)
intensional equality(直観主義的等価性？)
definitional equality
宇宙の記述のスタイルはTarski-style？
タルスキ宇宙
数式の[...]内はローカルコンテキストに相当
T(u) = U
$ \mathrm{Type} = \mathrm{Type} に相当するらしい
T(a)
El(a)
table:訳
immediate subtree
normal
contradiction 矛盾
確認用
Q.
#論文読み #論文 #文献